YES 1.464 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((readInt :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])]) :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\ndn * radix + d

is transformed to
readInt0 radix n d = n * radix + d

The following Lambda expression
\vu77
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt1 radix digToInt vu77 = 
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

The following Lambda expression
\vu68
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull0 vu68 = 
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule Main
  ((readInt :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])]) :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt10 radix digToInt (ds,r) = (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
readInt10 radix digToInt _ = []

The following Case expression
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull00 (cs@(_ : _),t) = (cs,t: []
nonnull00 _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ BR

mainModule Main
  ((readInt :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])]) :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)

is replaced by the following term
vy : vz

The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((readInt :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])]) :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

span3 p [] = ([],[])
span3 xx xy = span2 xx xy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((readInt :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])]) :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

are unpacked to the following functions on top level
span2Ys xz yu = span2Ys0 xz yu (span2Vu43 xz yu)

span2Span0 xz yu p ww wx True = ([],ww : wx)

span2Zs xz yu = span2Zs0 xz yu (span2Vu43 xz yu)

span2Vu43 xz yu = span xz yu

span2Ys0 xz yu (ys,wy) = ys

span2Zs0 xz yu (wz,zs) = zs

span2Span1 xz yu p ww wx True = (ww : span2Ys xz yu,span2Zs xz yu)
span2Span1 xz yu p ww wx False = span2Span0 xz yu p ww wx otherwise



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ Narrow

mainModule Main
  (readInt :: Int  ->  (Char  ->  Bool ->  (Char  ->  Int ->  [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs(yv4, :(yv610, yv611)) → new_span2Zs0(yv4, yv610, yv611)
new_span2Zs0(yv4, yv610, yv611) → new_span2Zs(yv4, yv611)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yv180), Succ(yv1500)) → new_primMinusNat(yv180, yv1500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv190), Succ(yv1500)) → new_primPlusNat(yv190, yv1500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv1400), Succ(yv300)) → new_primMulNat(yv1400, Succ(yv300))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(yv3, yv14, yv5, yv4, yv610, yv611, yv12) → new_foldl0(yv3, yv14, new_pt(yv5, yv610), yv5, yv4, yv611)
new_foldl1(yv3, yv14, yv15, yv5, yv4, yv6110, yv6111) → new_foldl(yv3, new_readInt0(yv3, yv14, yv15), yv5, yv4, yv6110, yv6111, new_span2Zs1(yv4, yv6111))
new_foldl0(yv3, yv14, yv15, yv5, yv4, :(yv6110, yv6111)) → new_foldl1(yv3, yv14, yv15, yv5, yv4, yv6110, yv6111)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_readInt0(Neg(yv30), Pos(yv140), yv15) → new_primPlusInt(yv140, yv30, yv15)
new_readInt0(Pos(yv30), Neg(yv140), yv15) → new_primPlusInt(yv140, yv30, yv15)
new_primPlusInt(yv140, yv30, Neg(yv150)) → Neg(new_primPlusNat0(new_primMulNat0(yv140, yv30), yv150))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusInt(yv140, yv30, Pos(yv150)) → new_primMinusNat0(yv150, new_primMulNat0(yv140, yv30))
new_readInt0(Neg(yv30), Neg(yv140), yv15) → new_primPlusInt0(yv140, yv30, yv15)
new_primPlusInt0(yv140, yv30, Pos(yv150)) → Pos(new_primPlusNat0(new_primMulNat0(yv140, yv30), yv150))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(yv180), Zero) → Pos(Succ(yv180))
new_primPlusInt0(yv140, yv30, Neg(yv150)) → new_primMinusNat0(new_primMulNat0(yv140, yv30), yv150)
new_readInt0(Pos(yv30), Pos(yv140), yv15) → new_primPlusInt0(yv140, yv30, yv15)
new_primMulNat0(Zero, Succ(yv300)) → Zero
new_primMulNat0(Succ(yv1400), Zero) → Zero
new_primMulNat0(Succ(yv1400), Succ(yv300)) → new_primPlusNat0(new_primMulNat0(yv1400, Succ(yv300)), Succ(yv300))
new_primPlusNat0(Zero, Succ(yv1500)) → Succ(yv1500)
new_primPlusNat0(Succ(yv190), Zero) → Succ(yv190)
new_primMinusNat0(Zero, Succ(yv1500)) → Neg(Succ(yv1500))
new_primPlusNat0(Succ(yv190), Succ(yv1500)) → Succ(Succ(new_primPlusNat0(yv190, yv1500)))
new_primMinusNat0(Succ(yv180), Succ(yv1500)) → new_primMinusNat0(yv180, yv1500)

The set Q consists of the following terms:

new_primPlusNat0(Zero, Succ(x0))
new_primPlusInt0(x0, x1, Neg(x2))
new_primPlusInt(x0, x1, Pos(x2))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusInt(x0, x1, Neg(x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_readInt0(Pos(x0), Neg(x1), x2)
new_readInt0(Neg(x0), Pos(x1), x2)
new_primMulNat0(Zero, Zero)
new_primPlusInt0(x0, x1, Pos(x2))
new_readInt0(Pos(x0), Pos(x1), x2)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Zero)
new_readInt0(Neg(x0), Neg(x1), x2)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: